Nuprl Lemma : add_mono_wrt_eq_rw
12,41
postcript
pdf
a
,
b
,
n
:
. {(
a
=
b
)
(
a
+
n
=
b
+
n
)}
latex
ProofTree
Definitions
{
T
}
Lemmas
add
mono
wrt
eq
origin
a, b, n:
. {(a = b) 
(a+n = b+n)}
a, b, n:. {(a = b) (a+n = b+n)}